$\forall$${\it ds}_{1}$, ${\it ds}_{2}$:$x$:Id fp$\rightarrow$ Type. ${\it ds}_{2}$ $\subseteq$ ${\it ds}_{1}$ $\Rightarrow$ State(${\it ds}_{1}$) $\subseteq\rho$ State(${\it ds}_{2}$)